Nuprl Definition : es-frame 0,22

es-frame(es;i;L;x;T) == vartype(i;x T & e@i(kind(e L (x after e) = (x when e
latex



clarification:

es-frame(es;i;L;x;T)
== es-vartype(esix T
== & alle-at(es;i;e.(es-kind(ese L  Knd)  es-after(esxe) = es-when(esxe T
latex


Definitionses-frame(es;i;L;x;T), A & B, vartype(i;x), e@iP(e), P  Q, A, (x  l), kind(e), Knd, (x after e), x when e
FDL editor aliaseses-frame

origin